The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We discuss some aspects of two-party and multi-party communication complexity theory. The topics include a sample from the long list of connections of communication complexity to other models of computation which provide strong motivation to the study of this subject; separation results for restricted models such as simultaneous and one-way communication; some counter-intuitive upper bounds in these...
This paper gives an overview of several results and techniques for graphs algorithms that compute the treewidth of a graph or that solve otherwise intractable problems when restricted graphs with bounded treewidth more efficiently. Also, several results on graph minors are reviewed.
It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as term-rewriting systems (which compute normal forms of input terms) and consider the case where individual systems share constructors, but not defined symbols. We present some old and new sufficient conditions under which termination (existence of normal forms, regardless of computation...
We describe constructions of several cryptographic primitives, including hash functions, public key cryptosystems, pseudo-random bit generators, and digital signatures, whose security depends on the assumed worst-case or average-case hardness of problems involving lattices.
Tiles are rewrite rules with side effects, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. They are well suited for modeling coordination languages, since they can be composed both statically and dynamically via possibly complex synchronization and work-flow mechanisms. In this paper, we give a the-based bisimilarity semantics for the asynchronous π-calculus of Honda and Tokoro...
The communication complexity of two-party protocols introduced by Abelson and Yao is one of the most intensively studied complexity measures for computing problems. This is a consequence of the relation of communication complexity to many fundamental (mainly parallel) complexity measures. This paper focuses on the relation between communication complexity and the following three complexity measures...
We prove lower bounds for a proof system having exponential speed-up over both polynomial calculus and constant-depth Frege systems in DeMorgan language.
A Stochastic Turing machine (STM) is a Turing machine that can perform nondeterministic and probabilistic moves and alternate between both types. Such devices are also called games against nature, Arthur-Merlin games, or interactive proof systems with public coins. We give an overview on complexity classes defined by STMs with space resources between constant and logarithmic size and constant or sublinear...
We prove an exponential lower bound for the length of any resolution proof for the same set of clauses as the one used by Urquhart [13]. Our contribution is a significant simplification in the proof and strengthening of the bound, as compared to [13]. We use on the one hand a simplification similar to the one suggested by Beame and Pitassi in [1] for the case of the pidgeon hole clauses. Additionally,...
We define a new logic query language, called DAC, which is an extension of Datalog. We exhibit queries which are not Datalog expressible but are DAC expressible. We also prove non-expressiveness results for DAC and we infer various strict hierarchies obtained by allowing more rapidly growing functions on the bound parameters.
A partially-observable Markov decision process (POMDP) is a generalization of a Markov decision process that allows for incomplete information regarding the state of the system. We consider several flavors of finite-horizon POMDPs. Our results concern the complexity of the policy evaluation and policy existence problems, which are characterized in terms of completeness for complexity classes. ...
Two categories are defined and their relationships are studied. The objects of the first category, PCOS, are prime coherent orthomodular posets, which have been mainly studied in connection with quantum logic. Morphisms in PCOS are homomorphisms in the usual sense, preserving order and a binary relation, named compatibility. The second category, denoted by LETS, comprises the class of labelled...
Timed models were introduced to describe the behaviors of real-time systems and, up to now, they were usually required to produce only executions with divergent sequences of times. However, some physical phenomena, as the movements of a damped oscillator, can be represented by convergent executions, producing Zeno words in a natural way. Moreover, time can progress if such an execution can be followed...
Ordered binary decision diagrams (OBDDs) have found a lot of applications in the verification of combinational and sequential circuits, protocols, and the synthesis and analysis of systems. The applications are limited, since the expressive power of polynomial-size OBDDs is too restricted. Therefore, several more general BDD models are used. Partitioned OBDDs are an OBDD model allowing a restricted...
We study hyper transition systems as a formalism to give semantics to specification languages which support both unbounded angelic and unbounded demonic non-determinism as well as recursion. Hyper transition are a generalization of transition systems and are suited for the specification of computations by means of properties that atomic steps in a computation have to satisfy. As an application we...
In this paper we discuss the meaning of sensitivity and its implications in CA behavior. A new shift-invariant metric is given. The metric topology induced by this metric is perfect but not compact. Moreover we prove that the new space is “suitable” for the study of the dynamical behavior of CA. In this context sensitivity assumes a stronger meaning than before (usually SZZ...
We present in this paper a subtyping extension of Calculus of Construction. We prove that this system has good meta-theoretical properties: transitivity elimination, subject reduction, strong normalization and decidability of subtyping. This work provides a theoretical foundation for adding subtyping to proof checkers like Coq, LEGO etc.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.